A:Type, I:MaInterface(A), i:Id.
(i  ma-interface-locs(I))  (k:Knd. (k  ma-interface-dom(I;i))  (hasloc(k;i))) 

latex

Definitions	Type, MaInterface(T), Id, ma-interface-dom(I;i), type List, {x:A| B(x)} , s = t, x:A. B(x), x:AB(x), t  T, P  Q, (x  l), Knd, b, x:A. B(x), A c B, x:A  B(x), left + right, , , A  B, A, False, s ~ t, ||as||, , SQType(T), {T}, l[i], SqStable(P), T, True, hasloc(k;i)
Lemmas	hasloc wf, assert wf, decidable assert, sq stable from decidable, Knd sq